p:PosetSig, a, b:|p|. (a <p b)  strict_part(x,y.x  y;a;b) 

latex

Up	sets 1
Definitions of Statement	a < b, a <p b
Definitions	t  T, x:A. B(x), a < b, strict_part(x,y.R(x;y);a;b), a <p b, True, T, P  Q, , P  Q, P & Q, x f y, P  Q
Lemmas	poset sig wf, set car wf, true wf, squash wf, assert of bnot, assert of set leq, and functionality wrt iff, assert of band, iff transitivity, not wf, set leq wf, bnot wf, set le wf, band wf, assert wf, iff functionality wrt iff